use "../Common/Core.sml";
use "../Common/CG.sig";

(* structure which implements a context graph data structure, including it's supported operations *) 
structure CG  = 
struct
	(* this "global" variable stores the number of hash table buckets in graphs created through the newGraph() function.  
	    in order to improve performance - it should be initialized to at least 2^X, where X is the number of variables in the analysed program. *)
	val numBuckets = ref 100;
 
	val debug = ref false;
	
	fun debugPrint(s) = if (!debug) then print(s) else ();
	
	(* a hash table structure with string keys *)
	structure HshTbl = 
      HashTableFn(struct
                    type hash_key = string
                    val hashVal = HashString.hashString
                    val sameKey = (op=) : string * string -> bool
				  end);
				  
	(* a variable set representation as a bit field *)
  	type Context = BitArray.array; 

	(* the data which is hanging on the context graph edges *)
	type edgeTag = sop_bar.DFR ref;

	(*the graph type - it is actually a hash table with string keys *)
	type graph = edgeTag HshTbl.hash_table;

	(* a tagged or untagged edge datatype *)
	datatype edge = E of Context * Context * edgeTag | UE of Context * Context;

	(* returns the specified edge's source context *)	
	fun edgeSrc(E (p,_,_)) = p
	  | edgeSrc(UE (p,_)) = p;

	(* returns the specified edge's target context *)		  
	fun edgeTgt(E (_,q,_)) = q
	  | edgeTgt(UE (_,q)) = q;

	(* creates a unique string key for the edge *)	  
	fun edgeToHash(e) = BitArray.toString(edgeSrc(e)) ^ "*" ^ BitArray.toString(edgeTgt(e));

	(* creates an untagged (UE) edge from a unique string key *)
	fun hashToEdge(hashStr : string) = 
		let
			val tokens = String.tokens (fn c => (c = #"*")) hashStr;	
		in
			UE (BitArray.fromString(hd tokens), BitArray.fromString(hd (tl tokens)))
		end;
	
	(* If dfr is non-empty:
	   1. edge exists in g - updates exiting edge's DFR to be: LUB(existing_DFR,  new_DFR) .
	   2. Otherwise, adds the new edge to g. *)
	fun addEdge(g : graph, e as E (_,_,dfr)) = 
		let
			val key = edgeToHash(e);
		in
			if (not (sop_bar.dfrEmpty(!dfr))) then
				( case (HshTbl.find g key) of SOME dfr' => (dfr' := sop_bar.sqcup(!dfr',!dfr))
														(* in case edge exist in graph update edge to be LUB(existing_DFR, new_DFR) *)
										    | NONE      => HshTbl.insert g (key, dfr) )
														(* Otherwise - insert new edge to g. *)
			else ()
		end;

	(* inserts a list of edges to the graph g. 
	    If a specified edge is already in g, the new edge's DFR will be joined with the existing edge's DFR *)
	fun addEdges(g : graph, []) = ()
	  | addEdges(g : graph, e::el) = (addEdge(g,e); addEdges(g,el));

  	(* constructor for new graphs - creates a new graph given the specified edge list *)
	fun newGraph([]) : graph = HshTbl.mkTable(!numBuckets, Fail "NotFound")
	  | newGraph(edgeList) : graph = 
			let
				val g = HshTbl.mkTable(!numBuckets, Fail "NotFound");
			in
				(addEdges(g,edgeList); g)
			end;
	
	(* returns the edge tag of the specified edge *)
	fun getEdgeTag(g : graph, UE(p,q) ) = HshTbl.find g (edgeToHash(UE (p,q)));

	(* returns a list of all edges in graph - not including edge tags (UE edge constructor is used to create each edge) *)	
	fun untaggedEdges(g : graph) =
		let
			fun rawListToEdgePairList([]) = []
			  | rawListToEdgePairList((hashStr,_)::t) = hashToEdge(hashStr)::rawListToEdgePairList(t);
		in
			rawListToEdgePairList(HshTbl.listItemsi(g))
		end;

	(* returns all edges in graph including edge tags (E edge constructor is usedto create each edge) *)
	fun edges(g : graph) =
		let
			fun rawListToEdgeList([]) = []
			  | rawListToEdgeList((hashStr,dfrRef)::t) = 
					let
						val UE(p,q) = hashToEdge(hashStr);
					in (
						E (p,q,dfrRef)) :: rawListToEdgeList(t)
					end;
		in
			rawListToEdgeList(HshTbl.listItemsi(g))
		end;
	(* creates an empty context which can hold up to the specified number of variables *)			
	fun makeEmptyContext(size : int) : Context = BitArray.bits(size, []);

	(* creates a context which can hold up to the specified number of variables and is filled with the specified list of variable indices *)
	fun makeContext(size : int, vars : int list) : Context = BitArray.bits(size, map (fn x => x-1) vars);

	(* returns a copy of the srcContext, assuming that numVars is the number of variables in srcContext *)
	fun copyContext(numVars, srcContext) = BitArray.bits(numVars, (BitArray.getBits(srcContext))); 
	
	(* adds variable with index x to context c *)
	fun addVarToContext(x, c) = BitArray.update(c, x-1, true); 

	(* removes variable with index x to context c *)	
	fun removeVarFromContext(x, c) = BitArray.update(c, x-1, false); 
	
	(* if 'add' is true - adds x to context c, otherwise removes x from context c *)
	fun setVarInContext(x, c, add) = if (add) then addVarToContext(x,c) else removeVarFromContext(x,c);

	(* returns a list of variable indices which are contained in the specified context. *)
	fun contextToVarList(c : Context) : int list = map (fn (x) => (x+1)) (BitArray.getBits(c));
	
 	(* outputs the context's variables to a nicely formatted string. *)	
	fun prtContext(vars) = 
		let fun prtVar(vars, index, comma) = if BitArray.sub(vars, index) then 
														(if (comma) then ", " else "") ^ Int.toString(index+1) 
											 else "";
		    fun prtVars(vars, index, len,first) = if (index < len) then 
																(let 
																    val var = prtVar(vars,index, not first);
																	val first1 = first andalso (String.size(var) = 0)
																 in 
																	var ^ prtVars(vars, index+1, len, first1) 
																 end)
															 else "";												 
		in
		    "{ " ^ prtVars(vars, 0, BitArray.length vars, true) ^ " }"
		end;

	fun prtContexts([]) = ""
	  | prtContexts(c::t) = prtContext(c) ^ ", " ^ prtContexts(t);
	  
	fun inContext(var : int, c : Context) = BitArray.sub(c, var-1);
	
 	(* a partial order on edges, based on lexicographic ordering of the source and target contexts. *)	
	fun edgeSmaller(e1,e2) = 
		let
			val p = BitArray.toString(edgeSrc(e1));
			val p' = BitArray.toString(edgeSrc(e2));
		in
			p < p' orelse (p = p' andalso (BitArray.toString(edgeTgt(e1)) < BitArray.toString(edgeTgt(e2))))
		end;

	(* inserts an edge into a sorted edge list *)
	fun insertEdge(e,[]) = [e]
	  | insertEdge(e,el as h::t) = if (edgeSmaller(h,e)) then h::insertEdge(e,t)
														 else e::el;
	(* sort an edge list by lexical order <src_context, tgt_context> *)
	fun sortEdges([]) = []
	  | sortEdges(e::t) = insertEdge(e,sortEdges(t));

	(* returns true iff context c1 is equal to context c2. *)		
	fun eqContexts(c1, c2) = BitArray.eqBits(c1,c2);

	fun contextSmaller(c1,c2) = 
		let
			val p = BitArray.toString(c1);
			val p' = BitArray.toString(c2);
		in
			p < p'
		end;
	
	fun insertContext(c,[]) = [c]
	  | insertContext(c,cl as h::t) = if ( contextSmaller(h,c)) then h::insertContext(c,t) else c::cl;
	  
	fun sortContexts(contextList) = foldl insertContext contextList [];

		(* returns all pre contexts of graph g. *)
	fun preContexts(g : graph) : Context list = map (fn UE(p,_) => p) (untaggedEdges(g));

	(* returns true if every context of preContextsList is a pre-contexts of graph g and vice-versa. *)	
	fun preContextsEqual(preContextsList, g) = 
		let
			fun equalContextLists([],[]) = true
			  | equalContextLists(_,[]) = false
			  | equalContextLists([],_) = false
			  | equalContextLists(c1::cl1, c2::cl2) = eqContexts(c1,c2) andalso equalContextLists(cl1,cl2);
		in
			equalContextLists(preContexts(g),preContextsList)
		end;
	
	(* returns true if every context of preContextsList is a pre-contexts of graph g. *)
	fun preContextsIn(preContextsLis, g) =
		let
			fun contextListIn([],[]) = true
			  | contextListIn(_,[]) = false
			  | contextListIn([],_) = true
			  | contextListIn(cl as c1::cl1, c2::cl2) = (eqContexts(c1,c2) orelse contextListIn(cl, cl2)) andalso contextListIn(cl1,cl2);
		in
			contextListIn(preContextsLis, preContexts(g))
		end;
		
	fun prtDfr(d as sop_bar.dfr(M,R)) = "\n    M=[ " ^ mat.prt(M) ^ "]\n    R=[ " ^ sop_bar.prtR(d) ^ "]";

	(* outputs the edge context variables and DFR to a nicely formatted string. *)		  
	fun prtEdge(E (p, q, d as (ref (sop_bar.dfr (M, R))))) = prtContext(p) ^ "-->" ^ prtContext(q) ^ " " ^ prtDfr(!d)
	  | prtEdge(UE (p, q)) = prtContext(p) ^ " ? "  ^ prtContext(q);

	(* for all edge in the list - outputs the edge context variables and DFR to a nicely formatted string. *)		  
	fun prtEdgeList([]) = ""
	  | prtEdgeList(e::t) = prtEdge(e) ^ "\n" ^ prtEdgeList(t);

 	(* for all edge in the graph - outputs the edge context variables and DFR to a nicely formatted string. *)	
	fun prtEdges(g : graph) =
		prtEdgeList(sortEdges(edges(g)))

	(* for all edge in the graph - outputs the edge context variables and DFR to a nicely formatted string. *)	
	fun printEdges(g : graph) =
		print(prtEdgeList(sortEdges(edges(g))))
	
	(* returns all post contexts of graph g. *)
	fun postContexts(g : graph) : Context list = map (fn UE(_,q) => q) (untaggedEdges(g));

	fun clone(g : graph) : graph = 
		newGraph(edges(g));

	(* returns true if g1 and g2 are equal in all aspects *)
	fun equal(g1 : graph, g2 : graph) =
		let
			fun equalLists([],[]) = true
			  | equalLists(_,[]) = false
			  | equalLists([],_) = false
			  | equalLists((E (p,q,d))::el1, (E (p',q',d'))::el2) = 
					eqContexts(p,p') andalso 
					eqContexts(q,q') andalso 
					sop_bar.dfrsame(!d,!d') andalso 
					equalLists(el1, el2);
		in
			equalLists( sortEdges(edges(g1)), sortEdges(edges(g2)) )
		end;
	
	(* returns true if c is a context which contains all variables (all bits are 1). *)
	fun isFullContext(c) = 
		let 
			val _ = BitArray.complement(c);
			val isFull = BitArray.isZero(c);
			val _ = BitArray.complement(c);
		in		
			isFull
		end;
	
	(* computes all possible contexts (except the full context) over a set of variables, 
	   where highestVar is the highest variable index *) 
	fun allContexts(highestVar) =
		let	
			fun intToBinaryInternal(0,n,k) = []
			  | intToBinaryInternal(i,n,k) = if ((i mod 2) = 1) then 
												(n-k+1)::intToBinaryInternal(i div 2,n,k-1) 
											 else 
											    intToBinaryInternal(i div 2,n,k-1) ;
			fun intToBinaryList(n) =
				intToBinaryInternal(n,n,n);
			
			fun makeAllContexts(highest_var,i) = 
				let
					val c = makeContext(highest_var, intToBinaryList(i));
				in
					 if (isFullContext(c)) then [] else  c :: makeAllContexts(highest_var,i+1)
				end;
			
			val l = makeAllContexts(highestVar,0);
			val _ = debugPrint("All contexts: " ^ prtContexts(l) ^ "\n");
		in
			l
		end;
	
		
	(* compute the composition of two graphs *)
	fun compose(g1 : graph, g2 : graph) = 
			let					
				fun composeSingle(e, []) = []
				  | composeSingle(e as E (p,q,dfr), l as (E (p',q',dfr'))::el) = 
						if (eqContexts(q,p')) then (E (p,q',ref (sop_bar.prod(!dfr,!dfr')))) :: composeSingle(e,el)
									else composeSingle(e,el);
									
				fun composeMultiple([], _) = []
				  | composeMultiple(e::el1, el2) = composeSingle(e,el2) @ composeMultiple(el1, el2);				
			in	
				newGraph( composeMultiple( edges(g1), edges(g2)  ) )
			end;
	
	(* computes the join (LUB) of two graphs *)	
	fun join(g1 : graph, g2 : graph) = 
			let
				val g1Edges = sortEdges(edges(g1));
				val g2Edges = sortEdges(edges(g2));
				val _ = debugPrint("Join:\ngraph 1:\n" ^ prtEdgeList(g1Edges));
				val _ = debugPrint("\ngraph 2:\n" ^ prtEdgeList(g2Edges));
				fun mergeEdgeLists([], el2) = el2
				  | mergeEdgeLists(el1, []) = el1
				  | mergeEdgeLists((e1 as E(p,q,d))::el1, (e2 as E(p',q',d'))::el2) = 
						if ( (eqContexts(p,p')) andalso (eqContexts(q,q')) ) then
							( E (p, q, ref (sop_bar.sqcup(!d, !d')) ) ) :: mergeEdgeLists(el1,el2)
						else
							(if (edgeSmaller(e1,e2)) then 
								e1::mergeEdgeLists(el1, e2::el2)
							 else
								e2::mergeEdgeLists(e1::el1, el2)
							 );
			in
				newGraph( mergeEdgeLists(g1Edges, g2Edges) )
			end;
			
end; (* struct CG *)

